Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | #include <stdlib.h> |
2 | #include <stdio.h> |
3 | #include <assert.h> |
4 | |
5 | #define LEN 10 |
6 | |
7 | extern unsigned __VERIFIER_nondet_uint(); |
8 | extern void __VERIFIER_assume(int); |
9 | |
10 | /* EXPLANATION |
11 | * The bug in this code is on line 20,the while loop |
12 | * The line needs to be (low <= high), so that the middle value isn't |
13 | * skipped when low and high converge |
14 | */ |
15 | |
16 | // Preconditions: |
17 | // arr is a sorted array |
18 | // size is the size of the array arr |
19 | int binary_search_function(int arr[], int size, int target) { |
20 | int low = 0; |
21 | int high = size - 1; |
22 | int mid; |
23 | while (low <= high) { |
24 | mid = (low + high)/2; |
25 | if (arr[mid] == target) { |
26 | return mid; |
27 | } |
28 | if (arr[mid] < target) { |
29 | low = mid + 1; |
30 | } |
31 | if (arr[mid] > target) { |
32 | high = mid - 1; |
33 | } |
34 | } |
35 | return -1; |
36 | } |
37 | |
38 | int dumb_sort(int arr[], int len, int target) { |
39 | for (int i=0; i<len; ++i) { |
40 | if (target == arr[i]) { |
41 | return i; |
42 | } |
43 | } |
44 | |
45 | return -1; |
46 | } |
47 | |
48 | int main() { |
49 | int arr[LEN] = { |
50 | __VERIFIER_nondet_int(), |
51 | __VERIFIER_nondet_int(), |
52 | __VERIFIER_nondet_int(), |
53 | __VERIFIER_nondet_int(), |
54 | __VERIFIER_nondet_int(), |
55 | __VERIFIER_nondet_int(), |
56 | __VERIFIER_nondet_int(), |
57 | __VERIFIER_nondet_int(), |
58 | __VERIFIER_nondet_int(), |
59 | __VERIFIER_nondet_int(), |
60 | }; |
61 | |
62 | int x = __VERIFIER_nondet_int(); |
63 | |
64 | for (int i=0; i<LEN-1; ++i) { |
65 | __VERIFIER_assume(arr[i] < arr[i+1]); |
66 | } |
67 | |
68 | int result = binary_search_function(arr, LEN, x); |
69 | printf("Result of binary search is = %d\n", result); |
70 | |
71 | // is the result correct? How can you check? |
72 | if (result != dumb_sort(arr, LEN, x)) { |
73 | assert(0); |
74 | } |
75 | |
76 | return 1; |
77 | } |
1 | #include <stdlib.h> |
2 | #include <stdio.h> |
3 | #include <assert.h> |
4 | |
5 | #define LEN 10 |
6 | |
7 | extern unsigned __VERIFIER_nondet_uint(); |
8 | extern void __VERIFIER_assume(int); |
9 | |
10 | /* EXPLANATION |
11 | * The bug in this code is on line 20,the while loop |
12 | * The line needs to be (low <= high), so that the middle value isn't |
13 | * skipped when low and high converge |
14 | */ |
15 | |
16 | // Preconditions: |
17 | // arr is a sorted array |
18 | // size is the size of the array arr |
19 | int binary_search_function(int arr[], int size, int target) { |
20 | int low = 0; |
21 | int high = size - 1; |
22 | int mid; |
23 | while (low <= high) { |
24 | mid = (low + high)/2; |
25 | if (arr[mid] == target) { |
26 | return mid; |
27 | } |
28 | if (arr[mid] < target) { |
29 | low = mid + 1; |
30 | } |
31 | if (arr[mid] > target) { |
32 | high = mid - 1; |
33 | } |
34 | } |
35 | return -1; |
36 | } |
37 | |
38 | int dumb_sort(int arr[], int len, int target) { |
39 | for (int i=0; i<len; ++i) { |
40 | if (target == arr[i]) { |
41 | return i; |
42 | } |
43 | } |
44 | |
45 | return -1; |
46 | } |
47 | |
48 | int main() { |
49 | int arr[LEN] = { |
50 | __VERIFIER_nondet_int(), |
51 | __VERIFIER_nondet_int(), |
52 | __VERIFIER_nondet_int(), |
53 | __VERIFIER_nondet_int(), |
54 | __VERIFIER_nondet_int(), |
55 | __VERIFIER_nondet_int(), |
56 | __VERIFIER_nondet_int(), |
57 | __VERIFIER_nondet_int(), |
58 | __VERIFIER_nondet_int(), |
59 | __VERIFIER_nondet_int(), |
60 | }; |
61 | |
62 | int x = __VERIFIER_nondet_int(); |
63 | |
64 | for (int i=0; i<LEN-1; ++i) { |
65 | __VERIFIER_assume(arr[i] < arr[i+1]); |
66 | } |
67 | |
68 | int result = binary_search_function(arr, LEN, x); |
69 | printf("Result of binary search is = %d\n", result); |
70 | |
71 | // is the result correct? How can you check? |
72 | if (result != dumb_sort(arr, LEN, x)) { |
73 | assert(0); |
74 | } |
75 | |
76 | return 1; |
77 | } |
1 | /* Macros and inline functions to swap the order of bytes in integer values. |
2 | Copyright (C) 1997-2020 Free Software Foundation, Inc. |
3 | This file is part of the GNU C Library. |
4 | |
5 | The GNU C Library is free software; you can redistribute it and/or |
6 | modify it under the terms of the GNU Lesser General Public |
7 | License as published by the Free Software Foundation; either |
8 | version 2.1 of the License, or (at your option) any later version. |
9 | |
10 | The GNU C Library is distributed in the hope that it will be useful, |
11 | but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
13 | Lesser General Public License for more details. |
14 | |
15 | You should have received a copy of the GNU Lesser General Public |
16 | License along with the GNU C Library; if not, see |
17 | <https://www.gnu.org/licenses/>. */ |
18 | |
19 | #if !defined _BYTESWAP_H && !defined _NETINET_IN_H && !defined _ENDIAN_H |
20 | # error "Never use <bits/byteswap.h> directly; include <byteswap.h> instead." |
21 | #endif |
22 | |
23 | #ifndef _BITS_BYTESWAP_H |
24 | #define _BITS_BYTESWAP_H 1 |
25 | |
26 | #include <features.h> |
27 | #include <bits/types.h> |
28 | |
29 | /* Swap bytes in 16-bit value. */ |
30 | #define __bswap_constant_16(x) \ |
31 | ((__uint16_t) ((((x) >> 8) & 0xff) | (((x) & 0xff) << 8))) |
32 | |
33 | static __inline __uint16_t |
34 | __bswap_16 (__uint16_t __bsx) |
35 | { |
36 | #if __GNUC_PREREQ (4, 8) |
37 | return __builtin_bswap16 (__bsx); |
38 | #else |
39 | return __bswap_constant_16 (__bsx); |
40 | #endif |
41 | } |
42 | |
43 | /* Swap bytes in 32-bit value. */ |
44 | #define __bswap_constant_32(x) \ |
45 | ((((x) & 0xff000000u) >> 24) | (((x) & 0x00ff0000u) >> 8) \ |
46 | | (((x) & 0x0000ff00u) << 8) | (((x) & 0x000000ffu) << 24)) |
47 | |
48 | static __inline __uint32_t |
49 | __bswap_32 (__uint32_t __bsx) |
50 | { |
51 | #if __GNUC_PREREQ (4, 3) |
52 | return __builtin_bswap32 (__bsx); |
53 | #else |
54 | return __bswap_constant_32 (__bsx); |
55 | #endif |
56 | } |
57 | |
58 | /* Swap bytes in 64-bit value. */ |
59 | #define __bswap_constant_64(x) \ |
60 | ((((x) & 0xff00000000000000ull) >> 56) \ |
61 | | (((x) & 0x00ff000000000000ull) >> 40) \ |
62 | | (((x) & 0x0000ff0000000000ull) >> 24) \ |
63 | | (((x) & 0x000000ff00000000ull) >> 8) \ |
64 | | (((x) & 0x00000000ff000000ull) << 8) \ |
65 | | (((x) & 0x0000000000ff0000ull) << 24) \ |
66 | | (((x) & 0x000000000000ff00ull) << 40) \ |
67 | | (((x) & 0x00000000000000ffull) << 56)) |
68 | |
69 | __extension__ static __inline __uint64_t |
70 | __bswap_64 (__uint64_t __bsx) |
71 | { |
72 | #if __GNUC_PREREQ (4, 3) |
73 | return __builtin_bswap64 (__bsx); |
74 | #else |
75 | return __bswap_constant_64 (__bsx); |
76 | #endif |
77 | } |
78 | |
79 | #endif /* _BITS_BYTESWAP_H */ |
1 | /* Inline functions to return unsigned integer values unchanged. |
2 | Copyright (C) 2017-2020 Free Software Foundation, Inc. |
3 | This file is part of the GNU C Library. |
4 | |
5 | The GNU C Library is free software; you can redistribute it and/or |
6 | modify it under the terms of the GNU Lesser General Public |
7 | License as published by the Free Software Foundation; either |
8 | version 2.1 of the License, or (at your option) any later version. |
9 | |
10 | The GNU C Library is distributed in the hope that it will be useful, |
11 | but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
13 | Lesser General Public License for more details. |
14 | |
15 | You should have received a copy of the GNU Lesser General Public |
16 | License along with the GNU C Library; if not, see |
17 | <https://www.gnu.org/licenses/>. */ |
18 | |
19 | #if !defined _NETINET_IN_H && !defined _ENDIAN_H |
20 | # error "Never use <bits/uintn-identity.h> directly; include <netinet/in.h> or <endian.h> instead." |
21 | #endif |
22 | |
23 | #ifndef _BITS_UINTN_IDENTITY_H |
24 | #define _BITS_UINTN_IDENTITY_H 1 |
25 | |
26 | #include <bits/types.h> |
27 | |
28 | /* These inline functions are to ensure the appropriate type |
29 | conversions and associated diagnostics from macros that convert to |
30 | a given endianness. */ |
31 | |
32 | static __inline __uint16_t |
33 | __uint16_identity (__uint16_t __x) |
34 | { |
35 | return __x; |
36 | } |
37 | |
38 | static __inline __uint32_t |
39 | __uint32_identity (__uint32_t __x) |
40 | { |
41 | return __x; |
42 | } |
43 | |
44 | static __inline __uint64_t |
45 | __uint64_identity (__uint64_t __x) |
46 | { |
47 | return __x; |
48 | } |
49 | |
50 | #endif /* _BITS_UINTN_IDENTITY_H. */ |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2025-05-12 | 21:22:15:368 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2025-05-12 | 21:22:15:454 | INFO | CPAchecker.run | CPAchecker 4.0 / default (OpenJDK 64-Bit Server VM 17.0.14) started |
| 2025-05-12 | 21:22:15:477 | INFO | CPAchecker.parse | Parsing CFA from file(s) "code.c" |
| 2025-05-12 | 21:22:16:770 | WARNING | CheckBindingVisitor.visit | Undefined function __VERIFIER_nondet_int found, first called in line 50 |
| 2025-05-12 | 21:22:18:003 | INFO | CoreComponentsFactory.createAlgorithm | Using heuristics to select analysis |
| 2025-05-12 | 21:22:18:017 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.callstack.unsupportedFunctions |
| 2025-05-12 | 21:22:18:017 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2025-05-12 | 21:22:18:029 | INFO | SelectionAlgorithm.chooseConfig | Performing heuristic ... |
| 2025-05-12 | 21:22:18:037 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties CoreComponentsFactory.createAlgorithm | Using Restarting Algorithm |
| 2025-05-12 | 21:22:18:049 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/parallel-valueAnalysis.properties ... |
| 2025-05-12 | 21:22:18:070 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 ResourceLimitChecker.fromConfiguration | Using the following resource limits: Thread CPU-time limit of 90s |
| 2025-05-12 | 21:22:18:433 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant). |
| 2025-05-12 | 21:22:18:631 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 InductionStepCase PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant). |
| 2025-05-12 | 21:22:18:658 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties RestartAlgorithm.run | Starting analysis 1 ... |
| 2025-05-12 | 21:22:18:996 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:19:361 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheckAlgorithm.checkCounterexample | Error path found, starting counterexample check with CPACHECKER. |
| 2025-05-12 | 21:22:19:762 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:866 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:878 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:885 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:896 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:902 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:906 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:932 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:950 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:19:968 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:20:107 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 PredicateCPA CtoFormulaConverter.getReturnType | line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:20:225 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:20:292 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:20:531 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheckAlgorithm.checkCounterexample | Error path found, starting counterexample check with CPACHECKER. |
| 2025-05-12 | 21:22:21:544 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:21:790 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck AutomatonGraphmlParser.getSpecAsProperties | Cannot map specification // This file is part of CPAchecker, // a tool for configurable software verification: // https://cpachecker.sosy-lab.org // // SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org> // // SPDX-License-Identifier: Apache-2.0 OBSERVER AUTOMATON AssertionAutomaton // This automaton detects assertions that may fail // (i.e., a function call to __assert_fail). INITIAL STATE Init; STATE USEFIRST Init : // Match standard calls to __assert_fail with nice message on violations. MATCH {__assert_fail($1, $2, $3, $4)} -> ERROR("assertion in $location: Condition $1 failed in $2, line $3"); // Match if assert_fail or assert_func is called with any number of parameters. MATCH {__assert_fail($?)} || MATCH {__assert_func($?)} -> ERROR("assertion in $location"); // Print warnings for other common error functions to warn users about potentially wrong specification. MATCH {assert($?)} && !CHECK(location, "functionName==assert") -> PRINT "WARNING: Function assert() without body detected. Please run the C preprocessor on this file to enable assertion checking." GOTO Init; MATCH {__VERIFIER_error($?)} && !CHECK(location, "functionName==__VERIFIER_error") -> PRINT "WARNING: Function __VERIFIER_error() is ignored by this specification. If you want to check for reachability of __VERIFIER_error, pass '--spec sv-comp-reachability' as parameter." GOTO Init; MATCH {reach_error($?)} -> PRINT "WARNING: Function reach_error() is ignored by this specification. If you want to check for reachability of reach_error, pass '--spec sv-comp-reachability' as parameter." GOTO Init; END AUTOMATON to property type. Will ignore it (would only be problematic if this were the termination property). |
| 2025-05-12 | 21:22:21:790 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck AutomatonGraphmlParser.getSpecAsProperties | Cannot map specification // This file is part of CPAchecker, // a tool for configurable software verification: // https://cpachecker.sosy-lab.org // // SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org> // // SPDX-License-Identifier: Apache-2.0 OBSERVER AUTOMATON AssertionAutomaton // This automaton detects assertions that may fail // (i.e., a function call to __assert_fail). INITIAL STATE Init; STATE USEFIRST Init : // Match standard calls to __assert_fail with nice message on violations. MATCH {__assert_fail($1, $2, $3, $4)} -> ERROR("assertion in $location: Condition $1 failed in $2, line $3"); // Match if assert_fail or assert_func is called with any number of parameters. MATCH {__assert_fail($?)} || MATCH {__assert_func($?)} -> ERROR("assertion in $location"); // Print warnings for other common error functions to warn users about potentially wrong specification. MATCH {assert($?)} && !CHECK(location, "functionName==assert") -> PRINT "WARNING: Function assert() without body detected. Please run the C preprocessor on this file to enable assertion checking." GOTO Init; MATCH {__VERIFIER_error($?)} && !CHECK(location, "functionName==__VERIFIER_error") -> PRINT "WARNING: Function __VERIFIER_error() is ignored by this specification. If you want to check for reachability of __VERIFIER_error, pass '--spec sv-comp-reachability' as parameter." GOTO Init; MATCH {reach_error($?)} -> PRINT "WARNING: Function reach_error() is ignored by this specification. If you want to check for reachability of reach_error, pass '--spec sv-comp-reachability' as parameter." GOTO Init; END AUTOMATON to property type. Will ignore it (would only be problematic if this were the termination property). |
| 2025-05-12 | 21:22:22:275 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant). |
| 2025-05-12 | 21:22:22:277 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant). |
| 2025-05-12 | 21:22:22:284 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA Repository.addMBean | Warning: Error during registration of management interface AbstractionPredicatesMBean (org.sosy_lab.cpachecker:type=predicate,name=AbstractionPredicates) |
| 2025-05-12 | 21:22:22:522 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:522 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_0 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:532 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:532 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_1 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:540 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:540 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_2 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:545 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:546 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_3 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:558 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:558 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_4 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:568 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:568 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_5 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:573 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:574 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_6 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:591 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:593 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_7 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:593 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:595 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:597 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_8 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:606 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | lines 49-60: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: __CPAchecker_TMP_9 = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:635 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:635 | WARNING | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheck PredicateCPA CtoFormulaConverter.getReturnType | line 62: Return type of function __VERIFIER_nondet_int is void, but result is used as type int: x = __VERIFIER_nondet_int(); |
| 2025-05-12 | 21:22:22:904 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:23:026 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 1 CounterexampleCheckAlgorithm.checkCounterexample | Error path found but identified as infeasible. |
| 2025-05-12 | 21:22:23:027 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 2 CounterexampleCheckAlgorithm.checkCounterexample | Error path found but identified as infeasible. |
| 2025-05-12 | 21:22:23:051 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 2 |
| 2025-05-12 | 21:22:23:052 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:23:066 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:23:067 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:23:159 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:23:527 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:23:614 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 3 |
| 2025-05-12 | 21:22:23:614 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:23:619 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:23:620 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:23:679 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:24:179 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:24:320 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 4 |
| 2025-05-12 | 21:22:24:321 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:24:328 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:24:328 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:24:395 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:24:907 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:25:157 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 5 |
| 2025-05-12 | 21:22:25:158 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:25:176 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:25:177 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:25:220 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:25:841 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:26:200 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 6 |
| 2025-05-12 | 21:22:26:201 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:26:205 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:26:205 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:26:244 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:26:754 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:27:108 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 7 |
| 2025-05-12 | 21:22:27:109 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:27:116 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:27:116 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:27:159 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:28:051 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:28:472 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 8 |
| 2025-05-12 | 21:22:28:473 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:28:476 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:28:478 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:28:586 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:29:321 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:29:787 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 9 |
| 2025-05-12 | 21:22:29:788 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:29:791 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:29:791 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:29:823 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:30:665 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:31:326 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 10 |
| 2025-05-12 | 21:22:31:326 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:31:422 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:34:285 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:34:906 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Running algorithm to create induction hypothesis |
| 2025-05-12 | 21:22:36:107 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 KInductionProver.check | Starting induction check... |
| 2025-05-12 | 21:22:36:865 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 11 |
| 2025-05-12 | 21:22:36:866 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.run | Creating formula for program |
| 2025-05-12 | 21:22:36:884 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2025-05-12 | 21:22:38:252 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties Parallel analysis 3 AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2025-05-12 | 21:22:38:589 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties Analysis /cpachecker/config/components/parallel-valueAnalysis.properties ParallelAlgorithm.handleFutureResults | /cpachecker/config/components/parallel-kInduction.properties finished successfully. |
| 2025-05-12 | 21:22:38:599 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties RestartAlgorithm.skipNextAnalysesIfRequired | Ignoring restart configuration '/cpachecker/config/components/recursion.properties' because condition if-recursive did not match. |
| 2025-05-12 | 21:22:38:600 | INFO | Analysis /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties RestartAlgorithm.skipNextAnalysesIfRequired | Ignoring restart configuration '/cpachecker/config/components/concurrency.properties' because condition if-concurrent did not match. |
| 2025-05-12 | 21:22:38:600 | INFO | CPAchecker.runAlgorithm | Stopping analysis ... |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Selection Algorithm statistics | ||
| Size of preliminary analysis reached set | 0 | |
| Used algorithm property | /cpachecker/config/components/configselection-restart-valueAnalysis-fallbacks.properties | |
| Program containing only relevant bools | 0 | |
| Relevant boolean vars / relevant vars ratio | 0.3704 | |
| Requires alias handling | 0 | |
| Requires loop handling | 1 | |
| Has a single loop | 0 | |
| Requires composite-type handling | 0 | |
| Requires array handling | 1 | |
| Requires float handling | 0 | |
| Requires recursion handling | 0 | |
| Relevant addressed vars / relevant vars ratio | 0.0000 | |
| Program containing external functions | true | |
| Number of all righthand side functions | 3 | |
| Restart Algorithm statistics | ||
| Number of algorithms provided | 3 | |
| Number of algorithms used | 3 | |
| Last algorithm used | /cpachecker/config/components/concurrency.properties | |
| Total time for algorithm 3 | 20.551s | |
| Parallel Algorithm statistics | ||
| Number of algorithms used | 3 | |
| Successful analysis | /cpachecker/config/components/parallel-kInduction.properties | |
| Statistics for | /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties | |
| ======================================================================================= | ||
| Time spent in analysis thread /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties | 0.002s | |
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 2.56 | sum: 407, count: 159, min: 0, max: 5 |
| Number of global variables per state | 0.00 | sum: 0, count: 159, min: 0, max: 0 |
| Number of assumptions | 84 | |
| Number of deterministic assumptions | 38 | |
| Level of Determinism | 45% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 159 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.017s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| AutomatonAnalysis (AssertionAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.084s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 551, count: 551, min: 1, max: 1 [1 x 551] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 145 | |
| Max size of waitlist | 14 | |
| Average size of waitlist | 4 | |
| Number of computed successors | 159 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 1 | |
| Number of times breaked | 1 | |
| Total time for CPA algorithm | 0.688s | Max: 0.688s |
| Time for choose from waitlist | 0.002s | |
| Time for precision adjustment | 0.065s | |
| Time for transfer relation | 0.540s | |
| Time for stop operator | 0.064s | |
| Time for adding to reached set | 0.009s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 1 | 100% |
| Time for counterexample checks | 3.670s | |
| Statistics for | /cpachecker/config/components/parallel-valueAnalysis-itp-end.properties | |
| ======================================================================================= | ||
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 1.58 | sum: 220, count: 139, min: 0, max: 4 |
| Number of global variables per state | 0.00 | sum: 0, count: 139, min: 0, max: 0 |
| Number of assumptions | 212 | |
| Number of deterministic assumptions | 50 | |
| Level of Determinism | 24% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 478 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.049s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| AutomatonAnalysis (AssertionAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.117s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 2034, count: 2034, min: 1, max: 1 [1 x 2034] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 417 | |
| Max size of waitlist | 9 | |
| Average size of waitlist | 2 | |
| Number of computed successors | 478 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 50 | |
| Number of times breaked | 4 | |
| Total time for CPA algorithm | 0.823s | Max: 0.359s |
| Time for choose from waitlist | 0.007s | |
| Time for precision adjustment | 0.114s | |
| Time for transfer relation | 0.611s | |
| Time for stop operator | 0.064s | |
| Time for adding to reached set | 0.011s | |
| ValueAnalysisRefiner statistics | ||
| Number of refinements | 4 | |
| Number of targets found | 4 | count: 4, min: 1, max: 1, avg: 1.00 |
| Time for completing refinement | 0.814s | |
| Number of root relocations | 0 | |
| Number of similar, repeated refinements | 0 | |
| Number of unique precision increments | 3 | |
| PathExtractor statistics | ||
| Total number of targets found | 0 | |
| ValueAnalysisPathInterpolator statistics | ||
| Time for interpolation | 0.062s | |
| Number of interpolations | 3 | |
| Number of interpolation queries | 11 | count: 133, min: 0, max: 3, avg: 0.08 |
| Size of interpolant | 0.08 | sum: 10, count: 133, min: 0, max: 2 |
| Number of sliced prefixes | 7 | count: 3, min: 1, max: 4, avg: 2.33 |
| Extracting infeasible sliced prefixes | 0.210s | |
| Selecting infeasible sliced prefixes | 0.017s | |
| CEGAR algorithm statistics | ||
| Number of CEGAR refinements | 4 | |
| Number of successful refinements | 3 | |
| Number of failed refinements | 0 | |
| Max. size of reached set before ref. | 139 | |
| Max. size of reached set after ref. | 1 | |
| Avg. size of reached set before ref. | 108.00 | |
| Avg. size of reached set after ref. | 1.00 | |
| Total time for CEGAR algorithm | 1.862s | |
| Time for refinements | 1.037s | |
| Average time for refinement | 0.259s | |
| Max time for refinement | 0.420s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 1 | 100% |
| Time for counterexample checks | 2.499s | |
| Statistics for | /cpachecker/config/components/parallel-kInduction.properties | |
| ============================================================================ | ||
| PredicateCPA statistics | ||
| Number of abstractions | 120 | 5% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 0 | 0% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 120 | 100% |
| Times precision was empty | 120 | 100% |
| Times precision was {false} | 0 | 0% |
| Times result was cached | 0 | 0% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 0 | 0% |
| Times result was 'false' | 0 | 0% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 64 | |
| BDD entailment checks | 0 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 170 | |
| Avg ABE block size | 121.23 | sum: 14548, count: 120, min: 72, max: 170 |
| Number of predicates discovered | 0 | |
| Time for post operator | 0.544s | |
| Time for path formula creation | 0.529s | |
| Time for strengthen operator | 0.055s | |
| Time for prec operator | 0.033s | |
| Time for abstraction | 0.000s | Max: 0.000s, Count: 120 |
| Solving time | 0.000s | Max: 0.000s |
| Model enumeration time | 0.000s | |
| Time for BDD construction | 0.000s | Max: 0.000s |
| Time for merge operator | 0.003s | |
| Time for coverage checks | 0.000s | |
| Total time for SMT solver (w/o itp) | 0.000s | |
| Total number of created targets for pointer analysis | 0 | |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| Bounds CPA statistics | ||
| Bound k | 11 | |
| Maximum loop iteration reached | 12 | |
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 1.91 | sum: 3941, count: 2066, min: 0, max: 5 |
| Number of global variables per state | 0.00 | sum: 0, count: 2066, min: 0, max: 0 |
| Number of assumptions | 830 | |
| Number of deterministic assumptions | 286 | |
| Level of Determinism | 34% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 2237 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.008s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| AutomatonAnalysis (AssertionAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.030s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 2237, count: 2237, min: 1, max: 1 [1 x 2237] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 2226 | |
| Max size of waitlist | 190 | |
| Average size of waitlist | 68 | |
| LoopstackSortedWaitlist | 3.17 | sum: 1692, count: 534, min: 0, max: 707 |
| ReversePostorderSortedWaitlist | 2.01 | sum: 1102, count: 547, min: 0, max: 698 |
| LoopIterationSortedWaitlist | 3.14 | sum: 1679, count: 534, min: 0, max: 707 |
| CallstackSortedWaitlist | 292.09 | sum: 3213, count: 11, min: 2, max: 1692 |
| Number of computed successors | 2237 | |
| Max successors for one state | 2 | |
| Number of times merged | 32 | |
| Number of times stopped | 32 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 1.372s | Max: 1.214s |
| Time for choose from waitlist | 0.080s | |
| Time for precision adjustment | 0.173s | |
| Time for transfer relation | 0.975s | |
| Time for merge operator | 0.011s | |
| Time for stop operator | 0.022s | |
| Time for adding to reached set | 0.069s | |
| BMC algorithm statistics | ||
| Time for BMC formula creation | 1.383s | |
| Time for final sat check | 4.203s | |
| Time for bounding assertions check | 1.272s | |
| Time for induction formula creation | 7.462s | |
| Time for induction check | 3.613s | |
| Other statistics | ||
| ================ | ||
| Parallel Algorithm statistics | ||
| Number of algorithms used | 3 | |
| Successful analysis | /cpachecker/config/components/parallel-kInduction.properties | |
| Statistics for | /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties | |
| ======================================================================================= | ||
| Time spent in analysis thread /cpachecker/config/components/parallel-valueAnalysis-NoCegar.properties | 0.002s | |
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 2.56 | sum: 407, count: 159, min: 0, max: 5 |
| Number of global variables per state | 0.00 | sum: 0, count: 159, min: 0, max: 0 |
| Number of assumptions | 84 | |
| Number of deterministic assumptions | 38 | |
| Level of Determinism | 45% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 159 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.017s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| AutomatonAnalysis (AssertionAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.084s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 551, count: 551, min: 1, max: 1 [1 x 551] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 145 | |
| Max size of waitlist | 14 | |
| Average size of waitlist | 4 | |
| Number of computed successors | 159 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 1 | |
| Number of times breaked | 1 | |
| Total time for CPA algorithm | 0.688s | Max: 0.688s |
| Time for choose from waitlist | 0.002s | |
| Time for precision adjustment | 0.065s | |
| Time for transfer relation | 0.540s | |
| Time for stop operator | 0.064s | |
| Time for adding to reached set | 0.009s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 1 | 100% |
| Time for counterexample checks | 3.670s | |
| Statistics for | /cpachecker/config/components/parallel-valueAnalysis-itp-end.properties | |
| ======================================================================================= | ||
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 1.58 | sum: 220, count: 139, min: 0, max: 4 |
| Number of global variables per state | 0.00 | sum: 0, count: 139, min: 0, max: 0 |
| Number of assumptions | 212 | |
| Number of deterministic assumptions | 50 | |
| Level of Determinism | 24% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 478 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.049s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| AutomatonAnalysis (AssertionAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.117s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 2034, count: 2034, min: 1, max: 1 [1 x 2034] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 417 | |
| Max size of waitlist | 9 | |
| Average size of waitlist | 2 | |
| Number of computed successors | 478 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 50 | |
| Number of times breaked | 4 | |
| Total time for CPA algorithm | 0.823s | Max: 0.359s |
| Time for choose from waitlist | 0.007s | |
| Time for precision adjustment | 0.114s | |
| Time for transfer relation | 0.611s | |
| Time for stop operator | 0.064s | |
| Time for adding to reached set | 0.011s | |
| ValueAnalysisRefiner statistics | ||
| Number of refinements | 4 | |
| Number of targets found | 4 | count: 4, min: 1, max: 1, avg: 1.00 |
| Time for completing refinement | 0.814s | |
| Number of root relocations | 0 | |
| Number of similar, repeated refinements | 0 | |
| Number of unique precision increments | 3 | |
| PathExtractor statistics | ||
| Total number of targets found | 0 | |
| ValueAnalysisPathInterpolator statistics | ||
| Time for interpolation | 0.062s | |
| Number of interpolations | 3 | |
| Number of interpolation queries | 11 | count: 133, min: 0, max: 3, avg: 0.08 |
| Size of interpolant | 0.08 | sum: 10, count: 133, min: 0, max: 2 |
| Number of sliced prefixes | 7 | count: 3, min: 1, max: 4, avg: 2.33 |
| Extracting infeasible sliced prefixes | 0.210s | |
| Selecting infeasible sliced prefixes | 0.017s | |
| CEGAR algorithm statistics | ||
| Number of CEGAR refinements | 4 | |
| Number of successful refinements | 3 | |
| Number of failed refinements | 0 | |
| Max. size of reached set before ref. | 139 | |
| Max. size of reached set after ref. | 1 | |
| Avg. size of reached set before ref. | 108.00 | |
| Avg. size of reached set after ref. | 1.00 | |
| Total time for CEGAR algorithm | 1.862s | |
| Time for refinements | 1.037s | |
| Average time for refinement | 0.259s | |
| Max time for refinement | 0.420s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 1 | 100% |
| Time for counterexample checks | 2.499s | |
| Statistics for | /cpachecker/config/components/parallel-kInduction.properties | |
| ============================================================================ | ||
| PredicateCPA statistics | ||
| Number of abstractions | 120 | 5% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 0 | 0% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 120 | 100% |
| Times precision was empty | 120 | 100% |
| Times precision was {false} | 0 | 0% |
| Times result was cached | 0 | 0% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 0 | 0% |
| Times result was 'false' | 0 | 0% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 64 | |
| BDD entailment checks | 0 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 170 | |
| Avg ABE block size | 121.23 | sum: 14548, count: 120, min: 72, max: 170 |
| Number of predicates discovered | 0 | |
| Time for post operator | 0.544s | |
| Time for path formula creation | 0.529s | |
| Time for strengthen operator | 0.055s | |
| Time for prec operator | 0.033s | |
| Time for abstraction | 0.000s | Max: 0.000s, Count: 120 |
| Solving time | 0.000s | Max: 0.000s |
| Model enumeration time | 0.000s | |
| Time for BDD construction | 0.000s | Max: 0.000s |
| Time for merge operator | 0.003s | |
| Time for coverage checks | 0.000s | |
| Total time for SMT solver (w/o itp) | 0.000s | |
| Total number of created targets for pointer analysis | 0 | |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| Bounds CPA statistics | ||
| Bound k | 11 | |
| Maximum loop iteration reached | 12 | |
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 1.91 | sum: 3941, count: 2066, min: 0, max: 5 |
| Number of global variables per state | 0.00 | sum: 0, count: 2066, min: 0, max: 0 |
| Number of assumptions | 830 | |
| Number of deterministic assumptions | 286 | |
| Level of Determinism | 34% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 2237 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.008s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| AutomatonAnalysis (AssertionAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.030s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 2237, count: 2237, min: 1, max: 1 [1 x 2237] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 2226 | |
| Max size of waitlist | 190 | |
| Average size of waitlist | 68 | |
| LoopstackSortedWaitlist | 3.17 | sum: 1692, count: 534, min: 0, max: 707 |
| ReversePostorderSortedWaitlist | 2.01 | sum: 1102, count: 547, min: 0, max: 698 |
| LoopIterationSortedWaitlist | 3.14 | sum: 1679, count: 534, min: 0, max: 707 |
| CallstackSortedWaitlist | 292.09 | sum: 3213, count: 11, min: 2, max: 1692 |
| Number of computed successors | 2237 | |
| Max successors for one state | 2 | |
| Number of times merged | 32 | |
| Number of times stopped | 32 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 1.372s | Max: 1.214s |
| Time for choose from waitlist | 0.080s | |
| Time for precision adjustment | 0.173s | |
| Time for transfer relation | 0.975s | |
| Time for merge operator | 0.011s | |
| Time for stop operator | 0.022s | |
| Time for adding to reached set | 0.069s | |
| BMC algorithm statistics | ||
| Time for BMC formula creation | 1.383s | |
| Time for final sat check | 4.203s | |
| Time for bounding assertions check | 1.272s | |
| Time for induction formula creation | 7.462s | |
| Time for induction check | 3.613s | |
| Other statistics | ||
| ================ | ||
| Code Coverage | ||
| Function coverage | 0.333 | |
| Visited lines | 466 | |
| Total lines | 472 | |
| Line coverage | 0.987 | |
| Visited conditions | 18 | |
| Total conditions | 18 | |
| Condition coverage | 1.000 | |
| CPAchecker general statistics | ||
| Number of program locations | 478 | |
| Number of CFA edges (per node) | 477 | count: 478, min: 0, max: 2, avg: 1.00 |
| Number of relevant variables | 27 | |
| Number of functions | 9 | |
| Number of loops (and loop nodes) | 3 | sum: 18, min: 4, max: 10, avg: 6.00 |
| Size of reached set | 2066 | |
| Number of reached locations | 452 | 95% |
| Avg states per location | 4 | |
| Max states per location | 121 | at node N50 |
| Number of reached functions | 3 | 33% |
| Number of target states | 0 | |
| Time for analysis setup | 2.540s | |
| Time for loading CPAs | 0.950s | |
| Time for loading parser | 0.313s | |
| Time for CFA construction | 1.245s | |
| Time for parsing file(s) | 0.409s | |
| Time for AST to CFA | 0.427s | |
| Time for CFA sanity check | 0.039s | |
| Time for post-processing | 0.186s | |
| Time for loop structure | 0.008s | |
| Time for AST structure | 0.000s | |
| Time for CFA export | 0.812s | |
| Time for function pointers resolving | 0.003s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.105s | |
| Time for collecting variables | 0.067s | |
| Time for solving dependencies | 0.003s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.030s | |
| Time for exporting data | 0.005s | |
| Time for Analysis | 20.579s | |
| CPU time for analysis | 33.150s | |
| Time for analyzing result | 0.000s | |
| Total time for CPAchecker | 23.128s | |
| Total CPU time for CPAchecker | 37.940s | |
| Time for statistics | 0.152s | |
| Time for Garbage Collector | 0.372s | in 63 runs |
| Garbage Collector(s) used | PS MarkSweep, PS Scavenge | |
| Used heap memory | 113MB ( 108 MiB) max; 57MB ( 54 MiB) avg; 136MB ( 130 MiB) peak | |
| Used non-heap memory | 67MB ( 64 MiB) max; 58MB ( 56 MiB) avg; 69MB ( 65 MiB) peak | |
| Used in PS Old Gen pool | 86MB ( 82 MiB) max; 36MB ( 35 MiB) avg; 86MB ( 82 MiB) peak | |
| Allocated heap memory | 235MB ( 224 MiB) max; 140MB ( 133 MiB) avg | |
| Allocated non-heap memory | 70MB ( 67 MiB) max; 62MB ( 59 MiB) avg | |
| Total process virtual memory | 5513MB ( 5257 MiB) max; 5394MB ( 5144 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.name | default |
| 2 | analysis.programNames | code.c |
| 3 | analysis.selectAnalysisHeuristically | true |
| 4 | cfa.useCFACloningForMultiThreadedPrograms | true |
| 5 | cpa.callstack.unsupportedFunctions | pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow,_longjmp,longjmp,siglongjmp,atexit |
| 6 | datarace.config | dataRaceAnalysis.properties |
| 7 | heuristicSelection.addressedRatio | 0.0 |
| 8 | heuristicSelection.complexLoopConfig | components/configselection-restart-valueAnalysis-fallbacks.properties |
| 9 | heuristicSelection.loopConfig | components/multipleLoopsConfig.properties |
| 10 | heuristicSelection.loopFreeConfig | components/configselection-restart-bmc-fallbacks.properties |
| 11 | heuristicSelection.singleLoopConfig | components/singleLoopConfig.properties |
| 12 | language | C |
| 13 | log.level | INFO |
| 14 | memorycleanup.config | smg-memorycleanup.properties |
| 15 | memorysafety.config | smg-memorysafety.properties |
| 16 | overflow.config | overflowAnalysis.properties |
| 17 | parser.usePreprocessor | true |
| 18 | specification | /cpachecker/config/specification/Assertion.spc |
| 19 | termination.config | terminationAnalysis.properties |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}